
\documentclass[runningheads]{llncs}
\hyphenation{evaluation}
\lefthyphenmin = 3
\righthyphenmin=4

\usepackage{amsmath}
\usepackage{txfonts}
\usepackage{stmaryrd}
\usepackage{amsfonts}

\usepackage{amssymb}
\setcounter{tocdepth}{3}
\usepackage{graphicx}
\usepackage{algorithmic, algorithm}

\usepackage{url}
\newcommand{\keywords}[1]{\par\addvspace\baselineskip
\noindent\keywordname\enspace\ignorespaces#1}

\begin{document}

\mainmatter  % start of an individual contribution

% first the title is needed
\title{A Refinement Methodology for Formal PLC Verification}

% a short form should be given in case it is too long for the running head
\titlerunning{}

% the name(s) of the author(s) follow(s) next
%
% NB: Chinese authors should write their first names(s) in front of
% their surnames. This ensures that the names appear correctly in
% the running heads and the author index.
%
\author{Hai Wan, Gang Chen, Xiaoyu Song, Ming Gu}
%
\authorrunning{}
% (feature abused for this document to repeat the title also on left hand pages)

% the affiliations are given next; don't give your e-mail address
% unless you accept that it will be published
\institute{}

\toctitle{} \tocauthor{} \maketitle


\begin{abstract}
Programmable logic controllers (PLCs) are widely used in embedded systems. A timer plays a pivotal
role in PLC real-time applications. In our previous work, a formalization of PLC programs with
TON-timers was presented in the theorem proving system Coq. The behavior of a timer was
characterized by a set of axioms at an abstract level. Two key points of the work were the abstract
model and its interpretation. In this paper, we extend our previous work. Firstly, a concrete model
is built and the correctness of the abstract model is proved based on the concrete model. Secondly,
the interpretation is generalized by the introduction of a mapping function. Both works are done in
a unified framework that we propose in the paper. The essence of the framework is the notion of
refinement relation. We also give the principles of the correctness proof. As a case study, we
reconsider the quiz machine program. The experiment results show the correctness of the framework.

\keywords{PLC, real-time systems, theorem proving, Coq, TON-timer, translation validation,
refinement relation}
\end{abstract}

\section{Introduction}

Programmable logic controllers (PLCs) are widely used for safety critical applications in various
industrial fields. The correctness and reliability of PLC programs are of great importance. Two
distinguished features of PLCs programs are the use of timers and the cyclic behavior mode. In our
previous work \cite{cg_Coq_PLCII}, we formally modeled and proved the correctness of a PLC program
with timer control. Timers are explicitly modeled by a set of axioms. The behavior of the model is
represented by a set of sequences (or traces) where a sequence is an ordered list of systems
states. Our model is at the scan cycle level, which means that each state in the sequence
represents a scan cycle. Comparing to the rung level model (i.e., each rung is represented by a
state in the sequence), the model we used is an abstract model. We discussed how to map the states
in the scan cycle level sequence to those in the rung level sequence. There are several mappings.
In order to ensure the correctness of the abstract model several constraints about the input PLC
programs were proposed. According to the rung level model, the correctness of the abstract model
was proved manually without a formal Coq proof. In this paper, we continue our work. Firstly we
generalize the idea of mapping. The direction of mappings in this paper is different, since they
are from the concrete model to the abstract model. Secondly we prove the correctness of the
abstract model formally in Coq. These two issues are solved in a unified framework whose essence is
the notion of refinement relation. The model in the previous work is an instance of the framework's
application.

Translation validation \cite{Pnueli98translationvalidation} is an approach to the verification of
translators. It is deployed to check whether the generated code is a correct implementation of the
source code. In this paper we choose this approach to prove the correctness of the abstract model.
In order to establish the refinement relation between two models, first a common semantic framework
for the representations of models is needed; second, a formal definition of refinement relation
should be defined based on the semantic framework. Because of the real-time nature and time related
properties of PLC programs, we extend the semantic framework of
 \cite{Pnueli98translationvalidation} by adding expressive power to represent the notion of time.
We adopt timed execution sequences \cite{TPM_TTS} as the common semantic base for the concrete and
abstract models. The behavior of the concrete (or abstract) model is modeled by a set of timed
execution sequences. The notion of refinement is then defined as a relation among sequences from
the two sets.

Our computational model is an extension of synchronous transition system (STS)
\cite{Pnueli98translationvalidation}. We call it timed STS. A timed STS consists of two parts: an
STS and additional predicates describing the behavior of timers \cite{cg_Coq_PLCII}. Concrete and
abstract models are built at different abstract levels. In each model, PLC timers are modeled
explicitly. Based on the structure of the model, instead of verifying all  timed state sequences to
show the refinement relation, it is enough to show that by proving there exists a refinement
relation between the synchronous transition systems and a refinement relation between the
additional predicates. For the transition systems part, the refinement relation can be checked by a
model checker or an automatic first order theorem prover. And for the time related part, by adding
several constraints to the PLC program, there is always a refinement relation. These constraints
are reasonable and well accepted by PLC programmers.

The use of refinement relation between the concrete model and the abstract model benefits us in at
least two ways:

\begin{enumerate}

\item It facilitates the modeling and verification of the given PLC source codes. The refinement relation
between the concrete and abstract models has very helpful properties that all properties which are
held in the abstract model are also satisfied by the concrete model. Hence, it is sufficient to do
the verification at the abstract level which makes the proof process much simpler.

\item In the code generation process, the refinement relation can be used in two directions: first,
the correctness of the implementation can be checked according to the relation; second, the
constraints learnt from the building process of refinement relation can be deployed to direct the
code generation process by adding certain constraints.

\end{enumerate}

The rest of the paper is organized as follows. In section \ref{related_work} we summarize the
related works. Section \ref{PLC_TIMERS} introduces PLC and its timers.  The formal definitions of
the computational model and refinement relation is given in section
\ref{comp_model_refinement_relation}. The principles of modeling PLC programs with timers as well
as the outline of how to prove the refinement relation are described in detail in section
\ref{modeling_PLC_with_Timers}. In section \ref{case_study} we use a simple PLC program to
illustrate our method. Finally section \ref{conclusion} concludes the paper.

\subsection{Related Works}
\label{related_work}

On the modeling and verification of PLC programs, the methods used can be divided into two main
directions: model checking and theorem proving. Based on the operational semantics, in
\cite{Mader99timedautomaton} PLC programs are translated into timed automata. They proposed two
ways to model timers: one is to treat timers as symbolic function block calls and the other is to
model timers as separate timed automata. Model checker UPPAAL is employed to verify the model. In
\cite{ProvingSequentialFunctionChartProgramsUsingAutomata}, timed automata are used to model
Sequential Function Chart programs. In their work, the use of timers is restricted -- each step is
associated with a timer and the timer is taken for guarding the transitions -- in other words they
didn't model timers in their most general forms. A special automaton that orients real-time systems
-- PLC-automata is developed to model the specifications of real-time applications. Structured Text
programs can be automatically generated from PLC-automata\cite{dierks01plcautomata}. They didn't
model PLC programs with timers, but use timers to implement PLC-automata. In
\cite{NBauer:Thesis:1998} condition/event systems are adopted to model PLC programs. There is an
assumption that timers can be started only at the beginning of the calculation phase. In
\cite{ModellingPLCLV} the Ladder Diagram programs are researched and time is treated implicitly.
Model checker SMV was used to verify the model. The methods mentioned above are all related to the
model checking technologies. In \cite{DBLP:journals/rts/KramerV97} theorem prover Isabelle/HOL
system was used to model and verify PLC programs. Module verification method is adopted in the
paper. They had a simple model of time, because they assumed the the current value increases
monotonously and there is no reset action during this process. No explicit model of a timer was
given. In \cite{SynSignalModelPLC}, the synchronous language SIGNAL is used to model Structured
Text and Function Block Diagram programs. They did not treat timer instructions.

The translation validation approach was used to ensure the correctness of the generated codes in
\cite{KMR-ppdp2005}. In \cite{TV_in_OPT_COML}, the approach was adopted to compares the
intermediate form of the program before and after each compiler pass and verify the preservation of
semantics. In \cite{DBLP:conf/etfa/PollmacherZH05}, the authors employed translation validation for
code-generators of PLCs. Comparing to their work, our definition of refinement relation is
different from theirs in two ways. First they did not have the sampling function. The introduction
of sampling function helps to build a refinement relation between two models and ensure that the
cyclic behavior of PLCs is modeled. Second their had a constraint ``$\phiup(I_A)\subseteq I_C$''
which means that the initial states of the abstract model are mapped to a subset of the initial
states of the concrete model. We think this is an obstacle in proving the correctness of the
abstract model, since it may make the abstract sequences cannot cover all the concrete sequences.
In Thomas F. Melham 's book \cite{HOLandHardwareVerification}, several types of abstraction were
discussed. We adopt the idea of sampling function used in the temporal abstraction.

\section{Programmable Logic Controller and Timers}
\label{PLC_TIMERS}
%\begin{figure}[]
%        \center\includegraphics[scale = 0.5]
%        {figs/structure_plc}
%        \caption{\label{structure_plc} PLC cycle}
%      \end{figure}
A PLC system typically consists of a CPU, a memory and input/output points through which the system
communicates with its outside environment. The execution of a PLC program is an infinite loop in
which each iteration is called scan cycle. Typically each scan cycle can be divided into three
phases:

\begin{enumerate}

\item \textbf{Input phase} during which PLC system reads the values of sensors and
copies them into memory which forms a snapshot of the environment. These values do not change
throughout the rest of the cycle. Input phase costs the same time in each scan cycle.

\item \textbf{Calculation phase} during which the PLC system
executes the instructions and writes the results into memory. At the beginning of each calculation
phase PLC system does some preparations, such as self-check and timer instructions (for the timers
whose base is 10ms). The preparations cost the same time.

\item \textbf{Output phase} during which PLC maps the results into actuators. Output phase costs
the same time in each scan cycle.

\end{enumerate}

There are five standard programming languages for PLC \cite{IEEC61131-3} among which the Ladder
Diagram (LD) is the most widely used programming language. In this paper, we only consider the LD
programs.

As an embedded system, the real-time aspect of PLC system is ensured by the use of
timers.\footnote{Since there are many different kinds of PLCs in the industry and the instructions
used in these PLCs are different from each other, in order to ease the discussion, we focus our
research on S7-200 which is a kind of PLC produced by Siemens. In some cases, time is ensured by
the use of interruptions. We do not consider these cases here.} There are mainly three kinds of
timers in S7-200 \cite{s7-200-manual}: TON-timer, TONR-timer, and TOF-timer. In this paper, we
focus on the TON-timers. The other two kinds of timers can be treated in a similar manner.
According to the user manual of S7-200, a TON-timer and its behavior are demonstrated in
Fig.\ref{ton_timer}. A TON-timer has two input ports: IN that indicates whether the timer is
enabled and PT that is the preset value of the timer. There are two output ports: one for the
current value and the other for the timer bit. The characteristics of a TON-timer are informally
described as follows:

\begin{enumerate}

\item A TON-timer counts time (i.e. increase its current value) when its IN is ON and it is updated.

\item A TON-timer's timer bit is OFF and current value is cleared when its IN is OFF.

\item If a TON-timer's current value is greater than or equal to its PT, its timer bit is ON.

\item A TON-timer continues counting after its PT is reached, and stops counting when the maximum
value 32767 is reached.

\end{enumerate}
A TON-timer has three resolutions: 1ms, 10ms, and 100ms. The behaviors of timers with different
resolutions are different. For the timer with time base of 1ms, it updates every 1ms asynchronously
to the scan cycle. In other words, the timer bit can be updated multiple times during one scan
cycle. For the 10ms timer, it only updates at the beginning of each scan cycle. For the 100ms
timer, its current value is updated only when the instruction is executed. The user manual
emphasizes that for the 100ms timer, its instruction should be executed one and only one time
during each cycle. In order to treat timers uniquely, an abstract timer model is proposed in
section


\begin{figure}[]
        \center\includegraphics[scale = 0.6]
        {figs/ton_timer}
        \caption{\label{ton_timer} TON timer and its behivour}
      \end{figure}

\section{The Computation Model and the Refinement Relation}
\label{comp_model_refinement_relation}

Given a set $\mathcal {V}$ of variables, a state $s$ is a type-consistent interpretation of
$\mathcal{V}$. $s(v)$ denotes the value of $v$ at state $s$. The set of all states over $\mathcal
{V}$ is denoted by $\sum$.

We adopt the definition of synchronous transition systems in \cite{Pnueli98translationvalidation}
with some modifications.

\begin{definition}
The following components define a \textbf{synchronous transition system} (STS) $S = (\mathcal{V},
\Theta, \rho)$:
\begin{itemize}

\item $\mathcal{V}$: A finite set of system variables.

\item $\Theta$ : An initial condition predicate over system states.

\item $\rho$ : A transition relation. $\rho$ is a predicate over two states. Given two states $s$ and $s'$,
$\rho(s,s')=true$ iff $s'$ is a possible successor state of $s$.

\end{itemize}

\end{definition}

Before we introduce the additional time-related predicates, we define the timed state sequences.

\begin{definition}

A \textbf{timed state sequence} $\varsigmaup = (\sigma, T)$ consists of an infinite sequence
$\sigma$ of states $\sigma_i \in \sum ~(i \ge 0)$, and an infinite sequence $T$ of corresponding
times $T_i \in N$ that satisfy the following conditions:

\begin{itemize}

\item \textbf{Monotonicity} $\forall i \ge 0$ $T_{i+1} \geq T_i$.

\item \textbf{Progress} $\forall n \in N$, $\exists i \geq 0, T_i > n$.

\end{itemize}

The set of all timed state sequences is denoted by $\varrhoup$.

Alternatively a timed sequence can be represented by a function of type $N \rightarrow (\sum \times
N)$. Intuitively giving the function an index it will output a state and its corresponding time at
the index.
\end{definition}

\begin{definition}

A \textbf{time related predicate} is a predicate of type $\varrhoup \to bool$ that refers to
component $T$ of a timed state sequence.

\end{definition}

In the modeling of PLC programs, the behavior of timers is model by a set of time related
predicates.

An STS together with a set of time related predicates form a computational model.

\begin{definition}

A \textbf{timed synchronous transition system }(timed STS), denoted by TS, is a pair $(S, {\cal
P})$ where $S$ is an STS and ${\cal P}$ is a set of time related predicates.

\end{definition}

Now we give the definition of timed execution sequences of the model.

\begin{definition}

Given an STS $S =(V, \Theta, \rho)$ and an associated timed STS $ST = (S, {\cal P})$ , a timed
execution sequence $\varsigmaup = (\sigma, T)$ of $TS$ is a \textbf{timed state sequence} that
satisfies the following conditions:

\begin{itemize}

\item \textbf{Initiation} : $\Theta(\sigma_0)$ holds.

\item \textbf{Consecution} : $\forall i \in N$, $\rho (\sigma_i,\sigma_{i+1})$ holds.

\item \textbf{Timing Relation} : $\forall p \in {\cal P}$, $p(\varsigmaup)$ holds.

\end{itemize}

The set of all timed execution sequences is denoted by $||TS||$.

\end{definition}

A PLC program can be modeled by a timed STS, since it can be divided into two parts: time-related
part and non-time-related part. The non-time-related part can be modeled by an STS, while the
time-related part can be modeled by a set of predicates. We will describe how to deal with PLC
programs with timers in the section \ref{modeling_PLC_with_Timers}.

The refinement relation of two timed STS is given below based on their timed execution sequences.

\begin{definition}
\label{def_refinement}

Given two timed STSs $A$ and $C$, and two functions $f:N\rightarrow N$ satisfying $\forall i:N,
f(i) < f (i+1)$ and $\phiup : \sum_C \rightarrow \sum_A$, \textbf{{$C$ is a refinement of $A$
relative to $f$ and $\phiup$}} iff $\forall \varsigmaup_C = (\sigma_C, T_C) \in ||C||, \exists
\varsigmaup_A = (\sigma_A, T_A) \in ||A||, \forall i \in N, \phiup(\sigma_C(f(i))) = \sigma_A(i)
\wedge T_C(f(i)) = T_A(i)$.

\end{definition}

\begin{figure}[]
        \center\includegraphics[scale = 0.65]
        {figs/def_refinement}
        \caption{\label{fig_def_refinement} The refinement relation between sequences}
      \end{figure}

Definition \ref{def_refinement} is illustrated graphically in Fig. \ref{fig_def_refinement}.
Intuitively, the function $f$ can be understood as a sampling function. It sets infinite
observation points in the timed execution sequences of system $C$. If $C$ is a refinement of $A$,
then for a sequence $\varsigmaup_C \in ||C||$, the sampled points in $\varsigmaup_C$ forms another
sequence $\varsigmaup_C'$ in which they keeps the same order as $\varsigmaup_C$. By applying
$\phiup$ point-wise to $\varsigmaup_C'$, a new sequence which belongs to $||A||$ can be obtained.

\begin{definition}
\label{def_refinement}

For systems $A$ and $C$, $A$ refines $B$ iff there exists two functions $f$ and $\phiup$ such that
$C$ is a refinement of $A$ relative to $f$ and $\phiup$.
\end{definition}

The problem of checking the correctness of the abstract model turns to a problem of checking
whether there is a refinement relation between abstract model and concrete model.



\section{Modeling and Verification of PLC Programs with Timers}
\label{modeling_PLC_with_Timers}

To model a PLC program, there are several key problems that need to be taken into consideration
 \cite{Mader00aclassification}: (1) how to identify the programming language fragments that are
used; (2) how to model the cyclic operation mode; (3) how to model the timer. Besides the above
three points, we also investigate the following issues : (1) what are the assumptions and
constraints that make the abstract model correct; (2) how the computation part is model and at what
abstract level. Further more, as mentioned in section \ref{comp_model_refinement_relation}, the
computation part can be divided into two sub parts: non-time-related part and time-related part. In
this section, we describe the main principles of how to model a PLC program as a timed STS. In the
following sections, we assume the timed STS we want to build is $ST = (S, H)$. We first introduce
the control flow graph of PLC programs which gives us a formal base for later discussions.

\subsection{The Structure Representations}
\label{structure_representation}

We first give some definitions about control flow graph (CFG).

\begin{definition}

Let CFG = (V, A) be a directed graph, where $V$ is the set of vertices and $A$ is the set of arcs.
The set $V$ is divided into two subsets $N$ and $E$ such that $N \cap E = \emptyset \wedge N \cup E
= V$. In the graph, vertices in $V$ are represented by cycles while vertices in $E$ are represented
by triangles. An arc that connects two vertices $u$ and $v$ is denoted by $(u,v)$.

CFGs satisfy that $\forall (u,v)\in A, (u\in N \wedge v\in E) \vee (u\in E \wedge v\in N)$.

A \textbf{path} $p = v_1~v_2~\cdots~v_n$ is a sequence of vertices such that $\forall i\in[1,n),
(v_i,v_{i+1})\in A$. For clarity, the vertex $e\in E$ in a path is represented by
``$\stackrel{\underrightarrow{e}}{ }$''. The \textbf{length} of  $p$ is $(n-1)$, denoted by $|p|$.
For all $i\in [1,|p|+1]$, the \textbf{$i$-th element} is denoted by $p_i$.

Vertex $u$ is \textbf{reachable} from vertex $v$ iff there is a path from $u$ to $v$ in the CFG.

For a set $O\subseteq E$, two vertices $v_1,v_2\in O$ are called \textbf{adjacent relative to $O$
and path $p$}, denoted by $adj(v_1, v_2, p, O)$, iff $v_1 = p_1 \wedge v_2 = p_{|p|+1} \wedge
(p-\{v1, v2\}) \cap O = \emptyset$. If $O$ is clear in the context, $O$ will be omitted in
expressions.

\end{definition}

Take the CFG $(c)$ in Fig. \ref{fig_adjacent} for example. If $O = \{e_1,e_3,e_5\}$, then $e_1$ and
$e_5$ are not adjacent relative to path $\stackrel{\underrightarrow{e_1}}{ } v_1
\stackrel{\underrightarrow{e_3}}{ } v_3 \stackrel{\underrightarrow{e_5}}{ }$, since $e_3$ is in the
path. $e_1$ and $e_3$ are adjacent relative to path $\stackrel{\underrightarrow{e_1}}{ } v_1
\stackrel{\underrightarrow{e_3}}{ } $.

\begin{figure}[]
        \center\includegraphics[scale = 0.92]
        {figs/fig_adjacent}
        \caption{\label{fig_adjacent} Abstract levels}
      \end{figure}


The control structure of a PLC program can be described by a CFG $g = ((N,E), A)$. Intuitively
vertices in $N$ are used to represent rungs in PLC programs and vertices in $E$ are used to
represent the observation points. As mentioned in section \ref{PLC_TIMERS}, each scan cycle
contains an input phase and an output phase. Hence, there are always two vertices in the CFG: one
is $v_i$ representing the input phase and the other is $v_o$ representing the output phase. $v_i$
($v_o$, resp.) is \textbf{input} (\textbf{output}, resp.) \textbf{related}. A vertex is
\textbf{timer related} if the rung it represents is a timer instruction.

For instance, the CFG of the program shown in Fig. \ref{quizmachine} is depicted in Fig.
\ref{cfg_quiz_mechine}. Vertex $v_0$ represents the preparation at the beginning of the calculation
phase. Each of the rest vertices denotes a rung in the program. Since there is no loop and branch
constructs in the calculation phase, the CFG is a simple cycle (Note the cyclic behavior of PLC).
Every vertex $v$ is associated with three sets:  $ref_v$, $def_v$, and $times_v$, where $ref_v$ is
the set of variables vertex $v$ refers to, $def_v$ is the set of variables vertex $v$ defines (or
may modify) and $times_v$ is the set of all possible time spans used to reach vertex $v$ from the
beginning of the calculation phase. Tab.\ref{tab_ref_def} shows the sets for each vertex. The
superscript $v$ of each variable in the $ref_v$ means the variable is defined at vertex $v$. For
instance, $m^1_1$ in $ref_2$ means $m_1$ used at vertex $v_2$ is defined at vertex $v_1$. We assume
the executions of each rung cost the same time 3ms.\footnote{The execution times for different
rungs can be different, but this doesn't effect the modeling and verification process.} Timer bits
are special variables in PLC. Comparing to other variables, their values can change multiple times
without explicit assignments. Hence, in the associated table a timer bit can occur in different
$def$ sets. CFG and the table form a formal representation of a PLC program's control structure.

\begin{figure}[]
        \center\includegraphics[scale = 0.86]
        {figs/cfg_quiz_mechine}
        \caption{\label{cfg_quiz_mechine} The CFG of the quiz machine program}
      \end{figure}


\begin{table}
 \caption{\label{tab_ref_def} $ref$s and $def$s for the CFG of quiz machine}
\begin{center}
\begin{tabular}{c| c| c |c }
\hline Vertex & $ref$ & $def$ & $times$\\

\hline
i & \{$$\} & \{$i_0,i_1,i_2,i_3$\} & \{0ms\}\\
0 & \{$$\} & \{$$\} & \{3ms\}\\
1 & \{$i_0^i,i_1^i,m^1_1$\} & \{$m_1$\} & \{6ms\}\\
2 & \{$m^1_1$\} & \{$t_1$\}  & \{9ms\}\\
3 & \{$t^2_1,i_2^i,m^6_5,m^1_1,m^3_2$\} & \{$m_2$\}  & \{12ms\}\\
4 & \{$t^2_1,i_3^i,m^6_5,m^1_1,m^4_3$\} & \{$m_3$\}  & \{15ms\}\\
5 & \{$t^2_1,i_4^i,m^6_5,m^1_1,m^5_4$\} & \{$m_4$\}  & \{18ms\}\\
6 & \{$m^1_1,m^3_2,m^4_3,m^5_4,m^6_5$\} & \{$m_5$\}  & \{21ms\}\\
7 & \{$m^3_2$\} & \{$o_1$\}  & \{24ms\}\\
8 & \{$m^4_3$\} & \{$o_2$\}  & \{27ms\}\\
9 & \{$m^5_4$\} & \{$o_3$\}  & \{30ms\}\\
10 & \{$t^2_1,m^6_5$\} & \{$o_0$\}  & \{33ms\}\\
o & \{$$\} & \{$$\}  & \{33ms\}\\
\hline

\end{tabular}
\end{center}
\end{table}

\subsection{Modeling PLC Programs}
\label{model_plc_programs}

The timed STS we want to construct can based on either the PLC program or an existing timed STS.
The model on which the construction is based  is called base model. A PLC program is associated
with a CFG. The timed STS is also associated with a CFG. Comparing to the CFG of the PLC program,
CFGs of the timed STSs are abstract. The CFG associated to the base model is denoted by
$g=((N,E),A)$ and $V = (N,E)$. The primed version of variables and notations indicates they belong
to the model under constructions. For example, we use $g'=((N',E'),A')$ to represent the CFG
associated to the model we are constructing.

There are two points we need to mention before we introduce the principles of building timed STSs:

\begin{itemize}

\item The consecution condition of the timed STS is a disjunction composed of a set of
clauses. Both the disjunction and the clauses are predicates over two states.

\item Each vertex in set $N$ of a CFG is associated with some computations. Its predecessors
(successors, resp.) can be understood as the points where we can observe the input (output, resp.)
values of the computations. Furthermore, these computations are represented by several clauses in
the disjunction.

\end{itemize}

\subsubsection{Selecting Observation Vertices}

According to $g$, we need to select several observation points, i.e., a set $O\subseteq N$. These
points can be understood as the sampling points. $O$ should satisfy the condition that there is no
loop between any two adjacent vertices in $O$, i.e., $\forall e_1~e_2 \in
O,|\{p|~adj(e_1,e_2,p)\}|$ is finite ($|\bullet|$ is the number of elements in $\bullet$). $g'$ can
be constructed based on $g$ and $O$. There is correspondence between $g$ and $g'$, which is denoted
by an relation $\alpha \subseteq V\times V'$. The associated table is calculated based on $\alpha$.
For all $v'\in V'$, if $v' \in N$, then $def'_{v'} = \bigcup_{(v,v')\in\alpha} def_v \bigwedge
ref'_{v'} = \bigcup_{(v,v')\in\alpha} ref_v \bigwedge times'_{v'} =
MIN_{(v,v')\in\alpha}(times_v)$. If vertex $v$ is timer (input, output, resp.) related, then for
each $v'$ such that $(v, v')\in\alpha$ is also timer (input, output, resp.) related.

For instance, assume the base CFG is $(c)$ in Fig. \ref{fig_adjacent}. If only $e_1$ is chosen as
the observation vertex, the result abstract CFG is $(a)$. If we choose $O= \{e_1,e_4,e_5\}$, an
abstract CFG $(b)$ is obtained. The $\alpha$ between $(c)$ and $(b)$ is
$\{(v_1,v_2'),(v_2,v_2'),(v_1,v_3'),(v_3,v_3'),(v_4,v_1'\\),(v_0,v_1'),(v_4,v_4'),(v_0,v_4')
,(e_1,e_1'),(e_4,e_2'), (e_5,e_3')\}$.


The set $O$ can be used to build the link between the base model and the new model. In other words,
the sampling function $f$ described in section \ref{comp_model_refinement_relation} can be
constructed based on them. In section \ref{case_study}, we will introduce two models. One selects
only one vertex and the other selects almost all vertices. Generally speaking, the more abstract
the model is, the easier the reasoning is.


\subsubsection{Non-Time-Related Part}

Based on base CFG and the operational semantics of PLC, the non-time-related part of the program
can be modeled by an STS. In STS, the transition relation $\rho$ is a disjunction. Each clause in
the disjunction is a predicate over two states. The problem of constructing the STS is then turned
into the problem of finding the clauses in the disjunction. Informally in CFG the computations
along the path connecting any two adjacent observation vertices is modeled by a clause in the
disjunction. A clause is also a predicate over two states. An informal clause generation algorithm
can be described as: for all $p~ (v_1~v_2 \in O)$ such that $adj(v_1,v_2,p)$, build a clause.

For example in Fig. \ref{fig_adjacent} assume $O = \{e_1,e_4,e_5\}$. Then the disjunction has four
clauses: (1) a clause representing computations along path $\stackrel{\underrightarrow{e_1}}{ }v_1
\stackrel{\underrightarrow{e_2}}{ } v_2 \stackrel{\underrightarrow{e_4}}{ }$ ; (2) a clause
representing computations along path $\stackrel{\underrightarrow{e_1}}{ }v_1
\stackrel{\underrightarrow{e_3}}{ } v_3 \stackrel{\underrightarrow{e_5}}{ } $ ; (3) a clause
representing computations along path $\stackrel{\underrightarrow{e_4}}{ }v_4
\stackrel{\underrightarrow{e_6}}{ } v_0 \stackrel{\underrightarrow{e_1}}{ }$ ; (4) a clause
representing computations along path $\stackrel{\underrightarrow{e_5}}{ }v_4
\stackrel{\underrightarrow{e_6}}{ } v_0 \stackrel{\underrightarrow{e_1}}{ }$. In the result
abstract CFG (i.e. $(b)$ in Fig. \ref{fig_adjacent}), $v'_2$ represents the first clause, $v'_3$
represents the second clause, $v'_1$ represents the third clause, and $v'_4$ represents the fourth
clause.

\subsubsection{Time-Related Part}

Particularly the time-related part is the activities of timers. As discussed in
\cite{cg_Coq_PLCII}, a TON-timer is modeled by three hypotheses:
\begin{itemize}

\item \textbf{(Reset)}. If the IN to the timer turns off, so does the timer bit.

\item \textbf{(Set)}. If the preset time period is passed and that the IN has been
kept ON during this period, then the timer bit will turn ON.

\item \textbf{(Set Reverse)}. If the timer bit turns ON, then its IN must have been
kept ON for a period larger than the preset time.

\end{itemize}
These hypotheses constitute the time related predicates part of the timed STS.

\subsubsection{Cyclic Behavior}

The cyclic behavior is ensured by showing the fact that for all $\varsigmaup \in ||ST||$ there
exists a input related vertex which is visited infinitely in $\varsigmaup$. We will describe how
the notion of ``visit'' is defined in section \ref{case_study}.

\subsubsection{Assumptions and Constraints}
\label{lab_constraints}

The PLC programs considered in this paper are programs without loops, i.e., if we remove vertices
$v_i$, $v_o$ and their associated arcs, the rest CFG is an acyclic directed graph.



For each timer, there is an accompanying set of constraints. In the following descriptions, we
assume there is only one timer $t$ in the program. For programs with multiple timers, the
constraints are the union of the constraints of each timer.

\begin{itemize}

\item $\forall (e_1~ e_m \in O) ~(p = \stackrel{\underrightarrow{e_1}}{ }v_1 \stackrel{\underrightarrow{e_2}}{
} \cdots v_{m-1} \stackrel{\underrightarrow{e_m}}{ }), adj(e_1, e_m, p) \wedge (\exists i, (1 \le i
< m) \wedge t \in def_{v_i}) \rightarrow (\exists! i, (1 \le i < m) \wedge t \in def_{v_i})$. This
formula describes that if $e_1$ and $e_m$ are adjacent relative to $p$ then the timer bit of $t$
can change at most once along path $p$ and changes at the same vertex in $p$.

\item $\forall (e_1~ e_m \in O) (1\le i < m)(p = \stackrel{\underrightarrow{e_1}}{ }v_1 \stackrel{\underrightarrow{e_2}}{
} \cdots v_{m-1} \stackrel{\underrightarrow{e_m}}{ }))~(p' = \stackrel{\underrightarrow{e_1}}{
}v_1' \stackrel{\underrightarrow{e_2'}}{ } \cdots v_{m-1}' \stackrel{\underrightarrow{e_m}}{ })),
adj(e_1, e_m, p)  \wedge (t \in def_{v_i})\rightarrow (\forall j, 1 < j < i \rightarrow e_j =
e_j')$. This formula describes that if $v_1$ and $v_m$ are adjacent relative to $p$ and $p'$ and
$v_i$ is the time instruction, then the sub-paths in $p$ and $p'$ that connect $e_1$ and $e_i$ are
the same.

\item $\forall (e_1~ e_m \in O)(1\le i < m)(p = \stackrel{\underrightarrow{e_1}}{ }v_1 \stackrel{\underrightarrow{e_2}}{
} \cdots v_{m-1} \stackrel{\underrightarrow{e_m}}{ }), adj(e_1, e_m, p) \wedge (t \in def_{v_i})
\rightarrow ((\forall j, i \le j < m \rightarrow ref(IN_t) \cap def_{v_j} = \emptyset) \vee
(\forall j, 1 \le j \le i \rightarrow ref(IN_t) \cap def_{v_j} = \emptyset))$. This formula
describes that the timer instruction is executed at vertex $i$ and the variables used in the timer
instruction doesn't change either from vertex $v_i$ to vertex $e_m$ or from vertex $e_1$ to $v_i$
in path $p$. $ref(IN_t)$ is the set of variables used to calculate IN of $t$. For example, in Fig.
\ref{quizmachine} $ref(IN_{t_1})=\{m_1\}$.

\end{itemize}

The constraints are used to prove the correctness of the abstract model. Informally, for any two
adjacent vertices $v_1,v_m \in O$ that have a timer related vertex $v_i$ between them (depicted in
Fig. \ref{fig_constraints}), the values used by the timer instruction are sampled at $e_i$ and the
output of the instruction can be observed at $e_{i+1}$. The constraints ensure that (1) the values
used by the timer instruction stay the same from $e_1$ and $e_i$ or from $e_i$ to $e_n$; (2) the
time interval from $e_1$ to $e_i$ is always the same; (3) the timer bit value changes only at
$v_i$. In the abstract model, the computations between $e_1$ and $e_n$ are abstracted and
represented by a single vertex $v'_2$. The constraints make the values used or output by the timer
instruction visible at $e'_1$ or $e'_2$.

\begin{figure}[]
        \center\includegraphics[scale = 0.93]
        {figs/fig_constraints}
        \caption{\label{fig_constraints} The use of Constraints}
      \end{figure}

The constraints should be derived from the timed STS. Hence they are not axioms but theorems in
Coq. Detailed explanations can be found in section \ref{case_study}.

\subsection{Outline of Refinement Proof}
\label{outline_proof}

Given two timed STSs $A$ and $C$ such that $A$ is built on $C$. $C$ is a refinement of $A$ iff the
sampled version of a sequence which belongs to $||C||$ also belongs to $||A||$. The theorems need
to be proved can be classified into four groups : (1) Theorems stated that sampled sequences
satisfy the initiation condition of $A$; (2) Theorems proving that sampled sequences satisfy the
consecution condition of $A$; (3)Theorems proving that sampled sequences satisfy the timed related
predicates of $A$; (4) Theorems proving that sequences of $||C||$ satisfy the constraints described
in section \ref{lab_constraints}. Fig. \ref{fig_proof_outline} shows the dependence among theorems
and hypotheses.

\begin{figure}[]
        \center\includegraphics[scale = 0.76]
        {figs/fig_proof_outline}
        \caption{\label{fig_proof_outline} Outline of the proof}
      \end{figure}

\subsubsection{Define Functions}

Define two functions: sampling function $f : N\rightarrow N$ and mapping function $\phiup : \sum_C
\rightarrow \sum_A$. Given a timed state sequence $\varsigmaup_C:N\rightarrow (\sum_C \times N)$ of
$C$, a timed state sequence $\varsigmaup_A:N\rightarrow (\sum_A \times N)$ can be obtained :
$\varsigmaup_A (i) = \phiup(\varsigmaup_C (f(i)))$. Let $\phiup \circ\varsigmaup_C\circ f$ denote
the result sequence by sampling.

\subsubsection{Prove the Sampled Sequence Satisfies Initiation Condition of $||A||$}

Given a timed state sequence $\varsigmaup_C$ of $C$, we need to prove that $\varsigmaup_A =
\phiup\circ\varsigmaup_C\circ f$ is a sequence satisfying $\Theta_A(proj_1(\varsigmaup_A(0))$.
$proj_1$ is a function to get the first element of a pair. The proof of the theorem depends on the
initiation and consecution conditions of $||C||$. Usually, the theorem is not difficult to prove.

\subsubsection{Prove the Sampled Sequence Satisfies Consecution Condition of $||A||$}

Given a timed state sequence $\varsigmaup_C$ of $C$, we need to prove that $\varsigmaup_A =
\phiup\circ\varsigmaup_C\circ f$ is a sequence satisfying $\forall i \in N$, $\rho_A
(proj_1(\varsigmaup(i),proj_1(\varsigmaup(i+1))$. The proof of the theorem depends on the
consecution conditions of $||C||$.

\subsubsection{State the Constraints}

A set of theorems describing the constraints described in section \ref{lab_constraints} should be
proved based on the initiation and consecution conditions of $||C||$.

\subsubsection{Prove the Sampled Sequence Satisfies the Time Related Predicate of $||A||$}

This proof is done based on the theorems describing constraints and timed related predicates of
$||A||$. If we prove the theorems directly on $STS_C$, a lot of irrelevant information is
introduced which makes the proof much more difficult. The theorems about the constraints can help
to remove the irrelevant information. In practice, they are useful.

\section{Case Study}
\label{case_study}

In this section, we describe a quiz machine program, which is used to demonstrate our proof
methodology and explain some basic notion of PLCs as well.

\subsection{Quiz Machine Program}
\label{example}

A quiz machine is an equipment used in a contest which involves a host and several players. The
host uses his buttons to start and reset a contest. Every player controls his button which is
associated with a light. The button is used for the player to vie to answer and the light is used
to indicate that the corresponding player has the chance to answer. After the host starts a
contest, the first player who presses his button will turn on an associated light. If more than one
players press the buttons at the same time, the machine should inform the host to restart another
contest. If during the predefined time there is no one pressing the button, the machine should
inform the host that time is out and keep all players' lights off even if some of them press their
buttons. The ladder diagram implementation of quiz machine with three players and a predefined time
of 3 seconds is shown in Fig. \ref{quizmachine}.

As shown in Fig. \ref{quizmachine}, a LD program consists of a sequences of rungs. There are 10
rungs in the example program. Each rung can be seen as a connection between logical checkers
(contacts or relays) and actuators (coils). For example, the first rung contains three relays (i.e.
$m_1$, $i_1$ and $i_0$) and one coil (i.e. $m_1$). Normally each rung has only one coil. If a path
can be traced between the left side of the rung and the coil, through ON contacts, the rung is true
and the output coil storage bit is ON. A normally open contact (-$|~|$-) is closed (ON) when its
bit is 1 and it's normally OFF. A normally closed contact (-$|/|$-) is closed (ON) when its coil is
0 and it's normally ON.

In the program, $m_1$ is used to indicate whether the contest begins. $m_2$, $m_3$, and $m_4$
denote whether play$_1$, play$_2$, or play$_3$ presses his button respectively. TON-timer $t_1$ is
used to record whether the time after the host presses start button is longer than the predefined
time. $m_5$ represents whether there is player that presses his button. $o_1$, $o_2$, and $o_3$ are
used to turn on the corresponding lights $l_1$, $l_2$, and $l_3$ respectively. $o_0$ denotes
whether the time is out.

Three time related program properties should be satisfied. The host presses the reset button and
after a while he presses the start button. Between the time he presses the start button and
timeout:

\begin{itemize}

\item if there is only one who first press his button, the corresponding light will turn on and
the other lights stay off;

\item if more than one players first press their buttons at the same, their lights will be turned on
and the other lights stay off;

\item if no one presses the button, the light indicating timeout will turn on and the other lights stay off.

\end{itemize}

\begin{figure}[]
        \center\includegraphics[scale = 0.45]
        {figs/quizmachine}
        \caption{\label{quizmachine} The Ladder Diagram of Quiz Machine}
      \end{figure}

In previous work, we built an abstract model of the quiz machine program. Based on the model, the
above properties were proved to be satisfied by the model. The existing abstract model is
syntactically different from a timed STS model. In order to use the  existing proof results, we
build a timed STS model which is proved semantically equivalent to the abstract model. Then we
construct a concrete model and prove the refinement relation between them. Finally we prove the
properties are also satisfied by the concrete model with the help of the refinement relation.

\subsection{The Concrete Model}

The concrete model is built on the LD program with the observation vertices set
$O=\{e_0,e_1,e_2,e_3,e_4,e_5,e_6,e_7,e_8,e_9,e_{10}\}$. The abstract CFG is $(c)$ in Fig.
\ref{cfg_quiz_mechine}. Thus we have the definition of $location$. $l_i$ is corresponding to $e_i$.
A timed execution sequence is a sequence of states. Given a sequence, the value of a variable is
accessible by its position (i.e. its index in the sequence). Hence variables are functions of type
$Position \to Prop$. Variable of type $program\_counter$ can be understood in two ways : (1) it is
used to record the observation vertex at the current position; (2) it is used to record the
instruction executed at the current position. The notion of time is introduced by type $Time\_c$.
Function $fc$ maps each position to a time and it satisfies the monotonic property.


\begin{figure}[]
        \center\includegraphics[scale = 0.80]
        {figs/abstract_cfg_quiz_mechine}
        \caption{\label{abstract_cfg_quiz_mechine} Abstract CFGs}
      \end{figure}

{\small
\begin{verbatim}
Inductive location : Set :=
  l0 | l1 | l2 | l3 | l4 | l5 | l6 | l7 | l8 | l9 | l10.
Definition Position := nat.
Definition Var_c := Position -> Prop.
Definition program_counter := Position -> location.
Definition Time_c := nat.
Variable fc : Position -> Time_c.
Hypothesis fc_monotonic : forall p, fc p < fc (S p).
\end{verbatim}
}

Then, we have the following definitions of variables. The system state consists of 16 variables :
$i_0,i_1,i_2,i_3,i_4,m_1,m_2,m_3,m_4,m_5,o_0,o_1,o_2,o_3,t_1$ and $pc$.

{\small
\begin{verbatim}
Variables i0 i1 i2 i3 i4 : Var_c.
Variables m1 m2 m3 m4 m5: Var_c.
Variables o0 o1 o2 o3 : Var_c.
Variable t1 : Var_c.
Variable pc : program_counter.
\end{verbatim}
}


Based on the above notations, the non-time-related part of the timed STS is modeled by hypotheses
$initial\_states\_c$ and $next\_states\_c$. In order to save space, notation $V = \{i_0, i_1, i_2,
i_3, i_4, m_1, m_2, m_3, m_4, m_5, o_0, o_1, o_2, o_3, t_1\}$ and $pres(U)=\bigwedge_{v\in U}(v' =
v)$ are used in the following expressions. $pres(U)$ means all variables in $U$ do not change their
values. From the non-time-related part, a CFG can be derived.

{\small
\begin{verbatim}
Definition initial_condition_c
  i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 pc t1:=
    ~i0/\~i1/\~i2/\~i3/\~i4/\~m1/\~m2/\~m3/\~m4/\~m5/\
    ~o0/\~o1/\~o2/\~o3/\~pc/\~t1.
Definition next_condition_c
  (i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3:Prop) l
  (t1 i0' i1' i2' i3' i4' m1' m2' m3' m4' m5' o0' o1' o2' o3':Prop)l' t1':=
  match l with
     l0 => l' =l1/\pres(V\{i0,i1,i2,i3,l})
    |l1 => m1'=((m1\/i0)/\(~i1))/\l'=l2/\pres(V\{m1,l})
    |l2 => l' =l3/\pres(V\{t1,l})
    |l3 => m2'=((m2\/(~t1/\i2/\~m5))/\m1)/\l'=l4/\pres(V\{m2,l})
    |l4 => m3'=((m3\/(~t1/\i3/\~m5))/\m1)/\l'=l5/\pres(V\{m3,l})
    |l5 => m4'=((m4\/(~t1/\i4/\~m5))/\m1)/\l'=l6/\pres(V\{m4,l})
    |l6 => m5'=((m2\/m3\/m4\/m5)/\m1)/\l'=l7/\pres(V\{m5,l})
    |l7 => o1'=m2/\l'=l8/\pres(V\{o1,l})
    |l8 => o2'=m3/\l'=l9/\pres(V\{o2,l})
    |l9 => o3'=m4/\l'=l10/\pres(V\{o3,l})
    |l10=> o0'=(t1/\~m5)/\l'=l0/\pres(V\{o0,l})
  end.

Hypothesis initial_states_c : initial_condition_c
  (i0 0) (i1 0) (i2 0) (i3 0) (i4 0) (m1 0) (m2 0) (m3 0) (m4 0)
  (m5 0) (o0 0) (o1 0) (o2 0) (o3 0) (pc 0) (t1 0).
Hypothesis next_states_c : forall p,
  next_condition_c (i0 p)(i1 p)(i2 p)(i3 p)(i4 p)(m1 p)(m2 p)(m3 p)(m4 p)
   (m5 p)(o0 p)(o1 p)(o2 p)(o3 p)(pc p)(t1 p)(i0 (S p))(i1 (S p))(i2 (S p))
   (i3 (S p))(i4 (S p))(m1 (S p))(m2 (S p))(m3 (S p))(m4 (S p))(m5 (S p))
   (o0 (S p))(o1 (S p))(o2 (S p))(o3 (S p))(pc (S p))(t1 (S p)).
\end{verbatim}
}



The time-related part of the timed STS is modeled by three hypotheses, since there is only one
timer in the program. We give the hypotheses about TON-timer $t_1$ directly, then give detail
explanations.

\begin{itemize}

\item \textbf{Reset}. If the timer instruction is executed at position $p$ and the timer's IN is
OFF at position $p$, then the timer bit will turn OFF at next position.


{\small
\begin{verbatim}
Hypothesis h_t1_reset_c : forall p, pc p=l2 -> ~m1 p -> ~t1 (S p).
\end{verbatim}
}

\item \textbf{Set}. Given two positions $p_1$ and $p_2$ at which the timer instruction is executed.
If the time interval between them is greater than or equal to $t1_PT_c$ which is the preset time of
the timer, as well as its $IN$ keeps ON during this period, then the timer bit will turn ON at next
position. {\small
\begin{verbatim}
Hypothesis h_t1_set_c : forall p1 p2, pc p1 = l2 -> pc p2 = l2 ->
  t1_PT_c <= fc p2 - fc p1 -> being_true_c m1 p1 p2 l2 pc->t1(S p2).
\end{verbatim}
}

\item \textbf{Set Reverse}. If the timer bit is ON at position $p_2$ and the timer instruction was
executed at the previous position, then there exists a position $p_1$ before $p_2$ such that the
time interval between $pred~p_1$ and $p_2$ is great than or equal to $t1_PT_c$ and during this
period its IN stays ON.
{\small
\begin{verbatim}
Hypothesis h_t1_true_c : forall p2, pc (pred p2) = l2 -> t1 p2 ->
  exists p1, pc p1 = l2 /\ t1_PT_c <= fc (pred p2) - fc p1 /\
    being_true_c m1 p1 (pred p2) l2 pc.
\end{verbatim}
}
\end{itemize}

Finally, we get a timed STS of the PLC program. Note that the model is constructed based on the
operational semantics of PLC programs.

\subsection{The Abstract Model}

In our previous work, we chose the beginning of each output phase as the interpretation location.
We have three possible interpretation locations: location at the begin of the output phase,
location at the begin of the input phase and location at the end of the input phase. Locations in
the calculation phase are not accessible because of the feature of the PLC systems. According to
the framework described in the paper, it is the same as we choose $e_{10}$ as the only observation
vertex in graph (c) (shown in Fig. \ref{abstract_cfg_quiz_mechine}). We give the definition of the
timed STS directly. It should be noticed that the program counter variable is omitted, since there
is only one vertex in the CFG.

\begin{itemize}

\item The non-time-related part:

{\small
\begin{verbatim}
Definition initial_condition_a
  i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 t1:=
  ~i0 /\ ~i1 /\ ~i2 /\ ~i3 /\ ~i4 /\ ~m1 /\ ~m2 /\
  ~m3 /\ ~m4 /\ ~m5 /\ ~o0 /\ ~o1 /\ ~o2 /\ ~o3 /\ ~t1.
Definition next_condition_a
(i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 t1 i0' i1' i2' i3' i4'
  m1' m2' m3' m4' m5' o0' o1' o2' o3' t1' : Prop) :=
    (m1' = ((i0' \/ m1) /\ ~ i1')) /\
    (m2' = (((~ t1' /\ i2' /\ ~ m5) \/ m2) /\ m1')) /\
    (m3' = (((~ t1' /\ i3' /\ ~ m5) \/ m3) /\ m1')) /\
    (m4' = (((~ t1' /\ i4' /\ ~ m5) \/ m4) /\ m1')) /\
    (m5' = (((m2' \/ m3' \/ m4') \/ m5) /\ m1')) /\
    (o1' = m2') /\
    (o2' = m3') /\
    (o3' = m4') /\
    (o0' = (t1' /\ ~ m5')).

Hypothesis initial_states_a:initial_condition_a
  (i0 0) (i1 0) (i2 0) (i3 0) (i4 0) (m1 0) (m2 0) (m3 0)
  (m4 0) (m5 0) (o0 0) (o1 0) (o2 0) (o3 0) (t1 0).
Hypothesis next_states_a:forall p,next_condition_a(i0 p)(i1 p)(i2 p)(i3 p)(i4 p)
  (m1 p)(m2 p)(m3 p)(m4 p)(m5 p)(o0 p)(o1 p)(o2 p)(o3 p)(t1 p)(i0(S p))
  (i1(S p))(i2(S p))(i3(S p))(i4(S p))(m1(S p))(m2(S p))(m3(S p))
  (m4(S p))(m5(S p))(o0(S p))(o1(S p))(o2(S p))(o3(S p))(t1(S p)).
\end{verbatim}
}

\item The time-related part:
{\small
\begin{verbatim}
Hypothesis h_t1_reset : forall c, ~ m1 c -> ~ t1 c.
Hypothesis h_t1_set :
  forall c1 c2, t1_PT <= f (pred c2) - f (pred c1) ->
    being_true m1 c1 c2 -> t1 c2.
Hypothesis h_t1_true :
  forall c2, t1 c2 -> exists c1, t1_PT<=f(pred c2)-f(pred c1)
    /\being_true m1 c1 c2.
\end{verbatim}
}
\end{itemize}




\subsection{Functions $f$ and $\phiup$}

In this case, $\phiup$ is simply an identity function, since the variables used at concrete and
abstract models are the same.

Because the abstract model is built based on the concrete model with the observation vertices set
$O=\{l_{10}\}$, the mapping function is defined as following, cf.\cite{HOLandHardwareVerification}.

{\small
\begin{verbatim}
Definition P x := pc x = l0.
Definition f_mapping_0_to_Prop (x:nat)(P:nat->Prop) :=
  (forall x', x' < x -> ~ P x') /\ P x.
Definition f_mapping_0_to := epsilon nat_non_empty (f_mapping_0_to_Prop P).
Definition f_mapping_S_n_to_Prop (n x:nat)(P:nat->Prop) :=
  (forall x', n < x' < x -> ~ P x') /\ P x /\ (n < x).
Definition f_mapping_S_n_to(n:nat):=
  epsilon nat_non_empty(f_mapping_S_n_to_Prop n P).

Fixpoint f_mapping (n : nat) :=
match n with
    0 => f_mapping_0_to
  | S p => f_mapping_S_n_to (f_mapping p)
end.
\end{verbatim}
}

Predicate $P$ that makes the definition of $f\_mapping$ more general is used to describe the
conditions under which the values along the concrete sequence can be sampled. If given another
program, the only required change is to give a proper definition of $P$. The sampled sequence is
obtained with the help of $abs$. For instance, the sampled sequence of $m_1$ is denoted by $(abs~
m_1)$.

{\small
\begin{verbatim}
Definition abs (T:Type)(v : Var_c)(n:nat):= v (f_mapping n).
\end{verbatim}
}


Based on the definition of $f\_mapping$, four important lemmas are proved.

{\small
\begin{verbatim}
Lemma f_mapping_before_0 : forall p, p < f_mapping 0 -> ~ P p.
Lemma f_mapping_point_to_l0 : forall n, P (f_mapping n).
Lemma f_mapping_no_l0_between:forall n p,f_mapping n<p<f_mapping(S n)->~P p.
Lemma f_mapping_monotony_Sn: forall n, f_mapping n < f_mapping (S n).
\end{verbatim}
}

\subsection{Cyclic Behavior}

In the CFG associated with a timed STS of a PLC program, there exists some vertices $V_i\subseteq
N$ that are input related. And as mentioned in section \ref{model_plc_programs}, each vertex in $N$
is associated with several clauses in the disjunction representing the consecution condition. By
checking its the clauses we can conclude whether a vertex $v\in N$ is input related, since the
input related vertices have a property that the input variables can change when they are executed.

For instance, the CFGs of the abstract model and the concrete model are shown in Fig.
\ref{abstract_cfg_quiz_mechine}. In CFG $(c)$ vertex $v_0$ is input related, because its associated
clause is ``$l_0 => l' =l_1\/\backslash pres(V\backslash \{i_0,i_1,i_2,i_3,l\})$''. The infinite
visit of $v_0$ is ensured by two points : (1) lemma $f\_mapping\_point\_to\_l0$ describes that the
sampling location $e_0$ is infinitely visited; (2) hypothesis $next\_states\_c$ describes that when
the system is at location $e_0$ $v_0$ is executed.

\subsection{Proof of Refinement Relation}

The final result we want to get is that for all properties that are held by the abstract model are
also held by the concrete model which is stated as the following theorem. In the theorem $P$ is a
property of the abstract model and sequences of form ``$abs~\bullet f\_mapping$'' are the sampled
sequences. By using this theorem, the properties we have proved are also satisfied by the concrete
model.

{\scriptsize
\begin{verbatim} Theorem refinement_relation_property :
 forall P: Var->Var->Var->Var->Var->Var->Var->Var->Var->Var->Var->Var->Var->Var->Var->Prop,
  (forall f : Cycle->Time, forall i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 t1 : Var,
   (initial_condition_a(i0 0)(i1 0)(i2 0)(i3 0)(i4 0)(m1 0)(m2 0)(m3 0)(m4 0)(m5 0)
    (o0 0)(o1 0)(o2 0)(o3 0)(t1 0))->
  (forall p : Cycle,next_condition_a (i0 p)(i1 p)(i2 p)(i3 p)(i4 p)(m1 p)(m2 p)(m3 p)(m4 p)
   (m5 p)(o0 p)(o1 p)(o2 p)(o3 p)(t1 p)(i0(S p))(i1(S p))(i2(S p))(i3(S p))(i4(S p))(m1(S p))
   (m2(S p))(m3(S p))(m4(S p))(m5(S p))(o0(S p))(o1(S p))(o2(S p))(o3(S p))(t1(S p)))->
  (forall c, ~ m1 c -> ~ t1 c) -> (forall c1 c2, t1_PT <= f (pred c2) - f (pred c1) ->
   being_true m1 c1 c2 -> t1 c2)  ->
  (forall c2,t1 c2 -> exists c1, t1_PT<=f(pred c2)-f(pred c1)/\being_true m1 c1 c2)->
  P i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 t1) ->
 P(abs i0 f_mapping)(abs i1 f_mapping)(abs i2 f_mapping)(abs i3 f_mapping)(abs i4 f_mapping)
  (abs m1 f_mapping)(abs m2 f_mapping)(abs m3 f_mapping)(abs m4 f_mapping)(abs m5 f_mapping)
  (abs o0 f_mapping)(abs o1 f_mapping)(abs o2 f_mapping)(abs o3 f_mapping)(abs t1 f_mapping).
\end{verbatim}
}


As outlined in section \ref{outline_proof}, we structure the proofs into the following components.

\subsubsection{Initiation and Consecution}

The theorem about the initiation which is not difficult to prove is stated below.

{\small
\begin{verbatim}
Theorem concrete_trace_sat_abs_init_condition:
  initial_condition_a (abs i0 f_mapping 0)(abs i1 f_mapping 0)(abs i2 f_mapping 0)
  (abs i3 f_mapping 0)(abs i4 f_mapping 0)(abs m1 f_mapping 0)(abs m2 f_mapping 0)
  (abs m3 f_mapping 0)(abs m4 f_mapping 0)(abs m5 f_mapping 0)(abs o0 f_mapping 0)
  (abs o1 f_mapping 0)(abs o2 f_mapping 0)(abs o3 f_mapping 0)(abs t1 f_mapping 0).
\end{verbatim}
}

The theorem about the consecution is stated below. To prove the theorem, based on the construction
of the abstract timed STS, it is enough to prove that $\forall (s_1~s_2\cdots s_m : \sum_C)(e_1~e_m
\in O)(p = \stackrel{\underrightarrow{e_1}}{ }v_1 \stackrel{\underrightarrow{e_2}}{ } \cdots
v_{m-1} \stackrel{\underrightarrow{e_m}}{ }), adj(e_1,e_2,p) \wedge (\forall i\in[1,m),c_i (s_i
s_{i+1})) \to disj_a (s_1~s_m)$ where $c_i$ is the clauses associated with $v_i$ and $disj_a$ is
the disjunction representing the consecution condition. This property can be verified by a model
checker or an automatic first order theorem prover.

{\small
\begin{verbatim}
Theorem concrete_trace_sat_abs_next_condition : forall p, next_condition_a
  (abs i0 f_mapping p)(abs i1 f_mapping p)(abs i2 f_mapping p)(abs i3 f_mapping p)
  (abs i4 f_mapping p)(abs m1 f_mapping p)(abs m2 f_mapping p)(abs m3 f_mapping p)
  (abs m4 f_mapping p)(abs m5 f_mapping p)(abs o0 f_mapping p)(abs o1 f_mapping p)
  (abs o2 f_mapping p)(abs o3 f_mapping p)(abs t1 f_mapping p)(abs i0 f_mapping(S p))
  (abs i1 f_mapping (S p))(abs i2 f_mapping (S p))(abs i3 f_mapping (S p))
  (abs i4 f_mapping (S p))(abs m1 f_mapping (S p))(abs m2 f_mapping (S p))
  (abs m3 f_mapping (S p))(abs m4 f_mapping (S p))(abs m5 f_mapping (S p))
  (abs o0 f_mapping (S p))(abs o1 f_mapping (S p))(abs o2 f_mapping (S p))
  (abs o3 f_mapping (S p))(abs t1 f_mapping (S p)).
\end{verbatim}
}

\subsubsection{Constraints}

The constraints mentioned in section \ref{lab_constraints} are formalized and proved based on the
concrete model. These constraints shows that along the path $\stackrel{\underrightarrow{e_{10}}}{ }
v_0 \stackrel{\underrightarrow{e_0}}{ } v_1 \cdots \stackrel{\underrightarrow{e_9}}{ } v_{10}
\stackrel{\underrightarrow{e_{10}}}{ }$, (1) the value of timer bit changes only at $v_2$, that is
to say the values of timer bit at $e_2$ and $e_{10}$ are the same; (2) the value of $m_1$ (i.e. the
value of the timer's IN) stays the same between $e_1$ and $e_{10}$. These facts are

{\small
\begin{verbatim}
Definition offset := 2.
Definition t1_loc := l2.

Lemma t1_loc_change_property:forall n p1 p2,p1=f_mapping n->p2=f_mapping(S n)->
  (forall p, p1 <= p < p2 -> pc p <>  t1_loc -> t1 (S p) = t1 p).
Lemma offset_is_t1_loc : forall n p1 p2,p1=f_mapping n ->
  p2 = f_mapping(S n)-> pc (offset + p1) = t1_loc.
Lemma offset_is_less : forall n p1 p2, p1 = f_mapping n ->
  p2 = f_mapping (S n) -> offset  < p2 - p1.
Lemma t1_loc_is_unique:forall n p1 p2, p1=f_mapping n->p2=f_mapping(S n)->
  forall p, p1 <= p < p2 -> p <> offset + p1 -> pc p <> t1_loc.
Lemma offset_change_property:forall n p1 p2,p1=f_mapping n->p2=f_mapping(S n)->
  forall p, offset + p1 <= p < p2 -> m1 (S p) = m1 p.
\end{verbatim}
}

\subsubsection{Time Related Predicates}

The following theorems are about the timed related predicates. They can be proved based on the
above theorems of constraints and timed related predicates of the concrete model.

{\small
\begin{verbatim}
Theorem concrete_trace_sat_abs_t1_reset :
  forall c, ~abs m1 f_mapping c->~abs t1 f_map
Lemma concrete_trace_sat_abs_t1_true :
  forall c2,abs t1 f_mapping c2->exists c1, t1_PT <= abs fc f_mapping (pred c2)
  - abs fc f_mapping (pred c1) /\ being_true (abs m1 f_mapping) c1 c2.
Theorem concrete_trace_sat_abs_t1_set :
  forall c1 c2, t1_PT <= abs fc f_mapping (pred c2)-abs fc f_mapping(pred c1)->
    being_true (abs m1 f_mapping) c1 c2 -> abs t1 f_mapping c2.
\end{verbatim}
}

\section{Conclusions}
\label{conclusion}

In this paper, we continue our work of modeling and verification of PLC programs. In our previous
work, a formalization of TON-timers of PLC programs was presented in the theorem proving system
Coq. The behavior of a timer was characterized by a set of axioms at an abstract level. The work
has two key aspects. One is that we build an abstract model of a PLC program. The other is that how
to interpret the abstract model based on a concrete model. In this paper, we extend our previous
work. Firstly, a concrete model is built and the correctness of the abstract model is proved based
on the concrete model. Secondly, the interpretation is generalized by the introduction of a mapping
function. Both works are done in a unified framework. The essence of the framework is the notion of
refinement relation. We also give the outline of the correctness proof. As a case study, we
reconsider the quiz machine program. The experiment result show the correctness of the framework.
This framework also provides abilities to build more concrete and more abstract models which still
keep the refinement relation. Our future work is to study how to get a more abstract model based on
a given property.

\bibliographystyle{splncs}
\bibliography{ref}

\end{document}
